\begin{tabbing}
ES0
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$E$:Type\+
\\[0ex]$\times$EqDecider($E$)
\\[0ex]$\times$$T$:(Id$\rightarrow$Id$\rightarrow$Type)
\\[0ex]$\times$$V$:(Id$\rightarrow$Id$\rightarrow$Type)
\\[0ex]$\times$$M$:(IdLnk$\rightarrow$Id$\rightarrow$Type)
\\[0ex]$\times$Top
\\[0ex]$\times$${\it loc}$:($E$$\rightarrow$Id)
\\[0ex]$\times$${\it kind}$:($E$$\rightarrow$Knd)
\\[0ex]$\times$${\it val}$:($e$:$E$$\rightarrow$eventtype(${\it kind}$;${\it loc}$;$V$;$M$;$e$))
\\[0ex]$\times$${\it when}$:($x$:Id$\rightarrow$$e$:$E$$\rightarrow$$T$(${\it loc}$($e$),$x$))
\\[0ex]$\times$${\it after}$:($x$:Id$\rightarrow$$e$:$E$$\rightarrow$$T$(${\it loc}$($e$),$x$))
\\[0ex]$\times$${\it sends}$:($l$:IdLnk$\rightarrow$$E$$\rightarrow$(Msg\_sub($l$;$M$) List))
\\[0ex]$\times$${\it sender}$:(\{$e$:$E$$\mid$ isrcv(${\it kind}$($e$)) \}$\rightarrow$$E$)
\\[0ex]$\times$${\it index}$:($e$:\{$e$:$E$$\mid$ isrcv(${\it kind}$($e$)) \}$\rightarrow\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$${\it sends}$(lnk(${\it kind}$($e$)),${\it sender}$($e$))$\parallel$}}$)
\\[0ex]$\times$${\it first}$:($E$$\rightarrow\mathbb{B}$)
\\[0ex]$\times$${\it pred}$:(\{${\it e'}$:$E$$\mid$ $\neg$${\it first}$(${\it e'}$) \}$\rightarrow$$E$)
\\[0ex]$\times$${\it causl}$:($E$$\rightarrow$$E$$\rightarrow$Prop)
\\[0ex]$\times$ESAxioms(\=$E$;$T$;$M$;\+
\\[0ex]${\it loc}$;${\it kind}$;${\it val}$;
\\[0ex]${\it when}$;${\it after}$;
\\[0ex]${\it sends}$;${\it sender}$;${\it index}$;
\\[0ex]${\it first}$;${\it pred}$;
\\[0ex]${\it causl}$)
\-\\[0ex]$\times$ESAtomAxiom\{i:l\}($T$;$\lambda$$i$,$k$. kindcase($k$; $a$.$V$($i$,$a$); $l$,$t$.$M$($l$,$t$) ))
\\[0ex]$\times$Top
\-
\end{tabbing}